(declare-fun var0 () String)
(declare-fun var1 () String)
(declare-fun var2 () String)
(declare-fun var3 () Int)
(declare-fun var4 () Int)
(declare-fun var5 () Int)
(declare-fun var6 () Bool)
(declare-fun var7 () Bool)
(declare-fun var8 () Bool)
(assert (str.contains (str.replace "vKMy2#V-zJ" var1 var2) (str.replace (str.substr var1 var5 var5) (str.replace var0 var1 var1) (str.at var1 var3))))
(assert (>= (str.len var1) (str.len var2)))
(assert (str.prefixof (str.replace var0 var2 var2) (str.substr var1 var4 var5)))
(assert (str.in.re (str.at "76ZEZHveVt" var5) (re.+ re.allchar)))
(check-sat)
